T:Type, R:(TT).
Linorder(T;x,y.R(x,y))  (a, b:T. (R(a,b))  strict_part(x,y.R(x,y);b;a)) 

latex

Up	rel 1, rel 1
Definitions	x,y. t(x;y), t  T, P  Q, P & Q, P  Q, x(s1,s2), P  Q, , x:A. B(x), strict_part(x,y.R(x;y);a;b), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), False, A, P  Q
Lemmas	linorder wf, strict part wf, not wf